e:rvc(l,tg,v).P(e;v) == e:E. isrcv(e) & lnk(e) = l & tag(e) = tg & P(e;val(e)) 

latex

---

clarification:

es-er(es; l; tg; e,v.P(e;v))
== e:es-E(es).
== es-isrcv(es; e) & es-lnk(es; e) = l  IdLnk & es-tag(es; e) = tg  Id & P(e;es-val(es; e)) 

latex

Definitions	x:A. B(x), E, b, isrcv(e), IdLnk, lnk(e), P & Q, Id, tag(e), val(e)
FDL editor aliases	es-er